Nuprl Definition : ma-rename 0,22
ma-rename(rx;ra;rt;M)
== mk-ma(rename(rx;1of(M));
== rename(k.kind-rename(ra;rt;k);1of(2of(M)));
== rename(rx;1of(2of(2of(M))));
== rename(ra;f,s,v. f((s o rx),v) o 1of(2of(2of(2of(M)))));
== rename(p.<kind-rename(ra;rt;1of(p)),rx(2of(p))>
== rename;f,s,v. f((s o rx),v) o 1of(2of(2of(2of(2of(M))))));
== rename(p.<kind-rename(ra;rt;1of(p)),2of(p)>
== rename;L.map(p.<rt(1of(p)),s,v. 2of(p)((s o rx),v)>;L) o 1of(2of(2of(2of(2of(2of(M)))))));
== rename(rx;L.map(k.kind-rename(ra;rt;k);L) o 1of(2of(2of(2of(2of(2of(2of(M))))))));
== rename(p.<1of(p),rt(2of(p))>
== rename;L.map(k.kind-rename(ra;rt;k);L) o 1of(2of(2of(2of(2of(2of(2of(2of(M)))))))));
== rename(k.kind-rename(ra;rt;k);L.map(rx;L) o 1of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))));
== rename(k.kind-rename(ra;rt;k);1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== rename(rx
== rename;L.map(k.kind-rename(ra;rt;k);L) o
== rename;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))))))) 
latex

clarification:

ma-rename(rx;ra;rt;M)
== mk-ma(fpf-rename(IdDeq;rx;1of(M));
== fpf-rename(KindDeq;k.kind-rename(ra;rt;k);1of(2of(M)));
== fpf-rename(IdDeq;rx;1of(2of(2of(M))));
== fpf-rename(IdDeq;ra;f,s,v. f((s o rx),v) o 1of(2of(2of(2of(M)))));
== fpf-rename(product-deq(Knd;Id;KindDeq;IdDeq);p.<kind-rename(ra;rt;1of(p)),rx(2of(p))>;f,s,v.
== f((s o rx),v) o 1of(2of(2of(2of(2of(M))))));
== fpf-rename(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);p.<kind-rename(ra;rt;1of(p)),2of(p)>;L.
== map(p.<rt(1of(p)),s,v. 2of(p)((s o rx),v)>;L) o 1of(2of(2of(2of(2of(2of(M)))))));
== fpf-rename(IdDeq;rx;L.map(k.kind-rename(ra;rt;k);L) o 1of(2of(2of(2of(2of(2of(2of(M))))))));
== fpf-rename(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);p.<1of(p),rt(2of(p))>;L.
== map(k.kind-rename(ra;rt;k);L) o 1of(2of(2of(2of(2of(2of(2of(2of(M)))))))));
== fpf-rename(KindDeq;k.kind-rename(ra;rt;k);L.map(rx;L) o
== f1of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))));
== fpf-rename(KindDeq;k.kind-rename(ra;rt;k);1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== fpf-rename(IdDeq;rx;L.map(k.kind-rename(ra;rt;k);L) o
== f1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))))))) 
latex

Definitionsmk-ma, Knd, f o g, product-deq(A;B;a;b), IdLnk, Id, IdLnkDeq, <a,b>, f(a), KindDeq, rename(r;f), IdDeq, g o f, map(f;as), x.A(x), kind-rename(ra;rt;k), 1of(t), 2of(t)
FDL editor aliasesma-rename

origin